In this section we describe the syntax and semantics  of \emph{Reaction Networks with Delays} (\rnd). 
A \rnd network is  composed of a set of species $\res$ governed by a set of reactions $\RS$.
We begin by giving some intuitions on  their  dynamics.

% \comment{remove figure}
% 
% \begin{figure}[t]
% \centering
% \includegraphics[width=0.7\textwidth]{decay.pdf}
%  \caption{Figure (a) depicts an example of degradation function that is discretized in Figure (b) into three levels (0,1 and 2) } \label{fig:decay}
% \end{figure}

Species in  \res represent the actors of the modeled system. In the example introduced above, we have concrete species such as aspartame and also  more abstract ones representing rates or concepts like glycemia. 
Species may have several \emph{expression} levels. Levels are determined  
by the observable behavior of  species,  \ie  they refer to a change in the capability of action of species. In the context of toxicology, they may   represent dosages. We assume,  for each species $s$, an arbitrary but finite number  $\setlev_s$ of levels. 
Each species $s$ is initialized at a certain  level $\level{s}$ and  it decays gradually as  time passes by. The duration  of the  decay may vary among levels. It is formalized by  a function that associates to each level  either $\omega$ (unbounded) or its finite duration:  $$\life_s:[0..\setlev_s-1] \to \nat^+ \cup \{\omega \}.$$
We set  $\life_s(0) = \omega $ and for all $i>0$,
  $\life_s(i) \neq \omega $, as the duration of the lowest level is the only one which is (and must be) unbounded\footnote{This is a non-restrictive hypothesis that is specific to the modeled scenario}. 
%As depicted in Figure \ref{fig:decay}, the enumeration of expression levels grows from right to left, from the lowest expression level $0$,  that may have an unbounded duration, to the highest level $2$. 
% As an example the levels of glycemia  are $0, 1, 2,3$ representing respectively the low, hunger,  equilibrium and high concentration of glucose in blood. The corresponding durations are
% $$
% \life_{glycemia}(0) = \omega \qquad
% \life_{glycemia}(1) = 8 \qquad
% \life_{glycemia}(2) = 8 \qquad  \life_{glycemia}(3) = 8. 
% $$

The evolution of species is governed by a set of reactions  \RS, each being of the form: \looseness=-1
\begin{equation}\label{eq:reaction}
\rho ::= \tuple{R_{\rho}, I_{\rho}, P_{\rho}}
%\tuple{(r_j, \level{j})_{j \in R}, (i_h, \level{h})_{h\in I}, (p_k, op)_{k \in P} }, 
\end{equation}
 where $R_{\rho}$ (reactants), $I_{\rho}$ (inhibitors) are sets of pairs $(s, \level{s})$ and $P_{\rho}$ (products) is a non empty set of pairs $(s, op)$, where $s\in \res$,  $\level{s} \in [0..\setlev_s-1]$ and $op  \in \{+,-\}$.
 Species can appear at most once in each set $R_{\rho}$, $I_{\rho}$ and $P_{\rho}$. They can be present in both $R_{\rho}$ and $I_{\rho}$ but they must occur with different levels. %$+$ defines increase and $-$ decrease of levels of products. 
We write $s \in R_{\rho}$ to denote  $(s, \cdot) \in R_{\rho}$ similarly for $I_{\rho}$ and $P_{\rho}$ and we omit index $\rho$ if it is clear from the context ($\rho = \tuple{R,I,P}$).
To each reaction we associate  a measure,    the \emph{response time} (a function $\dur: \RS \to \nat^+$),  that characterizes the time required for yielding increase (+) and/or decrease (-) of  levels of products.  
%For instance (from Example \ref{ex:glucose}) we have reaction $\rho_7 = \tuple{\{(Insulin,1)\},\{ (Glycemia,2)\}, \{(Glycemia,-)\}}$ with $\dur(\rho_7)=2$ where $Insulin$ is a reactant, and $Glycemia$ plays at the same time the role of inhibitor and product.

\begin{example}[Glucose metabolism]\label{ex:glucose}
Take the example described in Section \ref{sec:example}.
 The set of species involved,  their expression levels and the corresponding decays are:
 $$ \begin{array}{llll}
\res = \{&
      Sugar &\setlev_{sugar}=\{0,1\} & \life_{sugar}(1)=2 \\
  &    Aspartame \quad &\setlev_{aspartame}=\{0,1\} & \life_{aspartame}(1)=2 \\
%  & Neurotransmitter \  &\setlev_{NT}=\{0,1\} & \life_{NT}(1)=2 \\
  & Glycemia &\setlev_{glycemia}=\{0,1,2,3\} \quad & \life_{glycemia}(1)=8 \\
  &&& \life_{glycemia}(2)=8\\
  &&& \life_{glycemia}(3)=8\\
  & Glucagon &\setlev_{glucagon}=\{0,1\} & \life_{glucagon}(1)=3\\
  &  Insulin &\setlev_{insulin}=\{0,1,2\} & \life_{insulin}(1)=3\\
  &&& \life_{insulin}(2)=3\\
    \end{array}
$$
 The levels of glycemia are: 0 corresponding to low, 1 to hunger, 2 to equilibrium and 3 to high. Likewise for insulin we have 0 that corresponds to inactive, 1 to low and 2 to high. All the levels for the other species are 0 for inactive and 1 for active.
The set of reactions $\RS = \{\rho_k=(R_k, I_k, P_k) \mid k\in [1..9]\}$ with corresponding response time\footnote{Decay and response times comply with the intuitive description given in Section \ref{sec:example} but do not follow any particular study on the subject.} $\dur_k$ is:
$$\begin{array}{l|c|c|c|l}
 \rho_k & Reactants \ R_k & Inhibitors \ I_k & Products \ P_k &  \dur_k \\
\hline
  \rho_1 \ & \{(Sugar,1)\} &\emptyset &\{(Insulin,+), (Glycemia,+)\} & 1\\
  \rho_2 & \{(Aspartame,1)\}& \emptyset &\{(Insulin,+)\} & 1\\
  \rho_3 & \emptyset &\{(Glycemia,1)\}& \{(Glucagon,+)\} &1\\
 % (\rho_4) & \{(Glycemia,1)\} &\{(Glycemia,2)\}& \{(NT,+)\} &1\\
 % (\rho_5) & \{(Glycemia,2)\} &\{(Glycemia,3)\}& \{(NT,-)\} &1\\
  \rho_4 & \{(Glycemia,3)\}& \emptyset& \{(Insulin,+)\} &1\\
  \rho_5 & \{(Insulin,2)\} & \emptyset &\{(Glycemia,-)\} &2\\
  \rho_6 & \{(Insulin,1), &&&\\
           & (Glycemia,3)\} & \emptyset &\{(Glycemia,-)\} &2\\
  \rho_7 & \{(Insulin,1)\} & \{ (Glycemia,2)\} &\{(Glycemia,-)\} &2\\
  \rho_{8} & \{(Glucagon,1)\} &\emptyset &\{(Glycemia,+)\} &2 %\ {\qed}
   \end{array}
 $$
\hfill $\diamond$
 \end{example} 



The dynamics of \rnd is formalized using  high-level Petri nets. Before specializing these nets, we describe the intended behavior of \rnd. We assume the existence of a unique discrete global clock that starts at zero, increments gradually and always shows the current date. This date is used as a timestamps to record changes in the level of species and as a reference to check the response time of reactions.
 
We represent the state of a species $s$ as a tuple $\tuple{\bool_s, \refr_s, \birth_s}$ where $\bool_s$ is an integer value storing  the current   level from zero to $\setlev_s -1$; $\refr_s$ is a timestamp recording the last date when the  level has been  updated; and $\birth_s$ is a tuple with $\setlev_s$ fields (one for each  level) each $\birth[i]$ containing   zero or a timestamp corresponding to level $i$. %We denote with $\birth[i]$ the content of field $i$ in $\birth$.
The system is initialized by setting the  level of all  species: \ie  each species $s$ is set to $\tuple{\level{s}, 0, 0^{\setlev_s} } $ where $\level{s}$ is the given initial  level and $0^{\setlev_s}$ denotes  the vector $\birth_s$ uniformly initialized with zero.
In the case of glucose, a possible initial state is  $\tuple{ 1, 0, [0,0,0]}$ (also denoted $\tuple{ 1, 0, 0^3}$).  

\rnd networks can evolve in two ways: 
\begin{enumerate}[{Case} 1.]


\item  \label{item:reaction} {\bf Reaction: }A reaction $\rho$ may happen if and only if all the reactants are available at least at the required  level and all the inhibitors are expressed at a level strictly inferior to the required one for the whole response time period $\dur(\rho)$. The triggering of a reaction results in the increase (+)  or decrease (-) of the  level of its products  by one.  
More precisely, assume a product $p$ at level $\lev_p$ and the clock at time $t$, in the case of +,  we pass from  $\tuple{\lev_p, \refr_p, \birth_p}$ to $\tuple{\lev_p + 1, t, \birth_p\sub{t}{\lev_p +1}}$.
Notice that we update $\birth_p[\lev_p+1]$ with  the current time $t$ to record the change to the new level.
In the case of -,  we pass from  $\tuple{\lev_p, \refr_p, \birth_p}$ to $\tuple{\lev_p - 1, t, \birth_p\sub{t}{\lev_p }}$.

\item \label{item:clock} {\bf Clock and Decay: }The date stored in the clock is incremented by one. As time passes by, species that are not sustained by a reaction, decay. 
A species may stay at  level $\lev$ for $\life(\lev)$ time units. 
Degradation happens as soon as the interval $\life(\lev)$ is elapsed and is obtained by decreasing the level to $\lev -1$, till reaching level zero.  
More formally,  if the clock indicates $t$, we pass from  $\tuple{\lev, \refr, \birth}$ to $\tuple{\lev - 1, t, \birth\sub{t}{\lev }}$, where the notation $\birth\sub{t}{\lev }$ means that we assign the timestamp $t$ at  position $\lev $ in $\birth$.
Observe that we update $\birth[\lev]$ with  the current time $t$ to indicate the last date when the species was at level $\lev$.


%\item {\bf Clock: } The date stored in the clock is incremented by one.


% \item \label{item:reclock} If a reaction $\rho$  requires a reactant  at  level $\level{}$ and the reactant is itself at level $\level{}$, then the reaction can be performed only if   $\life(\level{})> \dur(\rho)$. %the reaction is enabled 
% That is because,  by the time $\dur(\rho)$ is elapsed, the reactant has decayed.   

\end{enumerate}

We now comment on some specific design choices concerning reactions:
\begin{itemize}
 \item the set of reactants and inhibitors $R \cup I $ is allowed to be empty. This accounts for modeling an environment that is continuously sustaining the production of a species. In this case the response time is ignored because not significant;  
 \item a species can appear in the same reaction simultaneously as a reactant and an inhibitor. In such a case, we require them to occur with  different levels: 
$$(\{(s,\level{})\} \cup R, \{(s, \level{}')\} \cup I , P )$$
where $\level{}< \level{}'$. This means that the reaction  can take place only if the level $\lev_s$ of $s$ belongs to the interval $\level{} \leq \lev_s < \level{}'$. In particular, if $s$ has to be present  in a reaction exactly at level $\level{}$, $s$ should appear as a reactant at level $\level{}$ %(that has to be present at least at level $\level{}$) 
and as inhibitor at level $\level{}'=\level{}+1$;% (that has to be at least at level strictly less than $\level{}+1$).
 \item  species can appear only once in the set of products $P$. This implies that a product cannot be increased and decreased in the same reaction.
\end{itemize}




 
 
 
\begin{remark}
As a direct consequence of the description of the evolutions of \rnd,  for each species $s$ that is currently at level $\lev_s$,
the tuple $\birth_s$ contains, for each level, a timestamp interpreted as follows: 
$$
\birth_s[i] = 
\begin{cases}
\begin{minipage}{7cm}
 the timestamp indicating the date when $s$ changed its level to  $i$
\end{minipage}
 &  \text{for }  0 \leq i \leq \lev_s\\
\\
\begin{minipage}{7cm}
  the timestamp indicating the last date when $s$ was at level $i$ or $0$ if $s$ has not yet reached $i$.
\end{minipage} 
& \text{for } \lev_s < i \leq \setlev_s-1              
\end{cases}
$$
\hfill $\diamond$
\end{remark}

It is also worth observing that if a species is continuously sustained  by some reactions then it remains available in the system at a certain  level for a period that could be longer than the corresponding decay time. This is witnessed by the fact that the values of fields $\birth[\lev]$ and $\refr$ can be different: the first representing the starting date of availability at level $\lev$ and the second the last date of update. 
\begin{example}

Suppose to have a species with 5 expressions levels from 0 to 4, with  decay time for each level as follows:
$$
\life(4) = 3 \qquad \life(3) = 1 \qquad  \life(2) = 2 \qquad  \life(1) = 4 \qquad  \life(0) = \omega.
$$
Let the species be initialized at  level 3 ($ \tuple{3, 0, [0,0,0,0,0]}$) and  modified according to the following scenario:
$$
\begin{array}{ll}
 \text{initialization} & \tuple{3, 0, [0,0,0,0,0]}  \\
 \text{time passes by, the species decays} & \tuple{2, 1, [0,0,0,1,0]} \\
  \text{one unit of time passes by with no effect} & \tuple{2, 1, [0,0,0,1,0]}\\
  \text{time passes by, the species decays} & \tuple{1, 3, [0,0,3,1,0]} \\
 \text{two units of time passes by with no effect} & \tuple{1, 3, [0,0,3,1,0]}\\
 \text{a reaction augments the level of the species by one} & \tuple{2, 5, [0,0,5,1,0]}\\
  \text{one unit of time passes by with no effect} & \tuple{2, 5, [0,0,5,1,0]}\\
   \text{a reaction reduces the level of the species by one}& \tuple{1, 6, [0,0,6,1,0]}. \qquad \diamond
\end{array}
$$
\end{example}



More formally, we now introduce the high-level Petri net modeling of \rnd.
Each species $s\in \res$ is modeled by a single place $q_s $ whose type   $ L(q_s)$ is the set of  tuples of the form  $\tuple{\lev_s, \refr_s, \birth_s}$, where $\lev_s \in [0..\setlev_s-1]$, $\refr_s \in \nat$, $\birth_s \in \nat^{\setlev_s}$. 
In order to cope with time aspects present in \rnd we introduce a special place $\Pclock$, a clock\footnote{
Here, we assume  only one clock  per network but in principle the number of clocks is not a limitation.}  that maintains the current (discrete) time, hence $L(\Pclock ) = \nat$. The clock (Figure \ref{fig:clock}) is initialized with zero, it is incremented by one  by transition $t_c$ and no other transition can change it. 
Transition $t_c$ is also responsible of the decay of species.  
Finally, every reaction $\rho$ is modeled with  a transition $t_{\rho}$ (Figure \ref{fig:reaction}). Moreover, to each transition  $t_{\rho}$ we associate a special place $q_{\rho}$ that is used to ensure that the same reaction is not executed more than once in the same time unit.
More detailed explanations for each type of transition follow Definition \ref{def:rs}. \looseness=-1
 
\begin{definition}[\rsd network]\label{def:rs}
 Given a  \rnd network $(\res, \RS)$ with initial state $(s, \level{s})$ for each $s \in \res$,  its  high-level Petri net representation is defined as  tuple $(Q, T, F, L, M_0)$ where $z, z', \lev, \lev', \refr, \refr', \birth, \birth', w, w'$ are variables and:
\begin{itemize} 
 \item $Q = \{\Pclock\} \cup \{q_s \mid  s \in{\res}\} \cup \{q_{\rho} \mid  \rho \in \RS \}; $
 \item $T= \{t_c \} \cup \{t_{\rho} \mid \rho \in \RS \}$;

 \item 
$  F=  \{ (q,t_c),(t_c, q) \mid q \in Q \} \quad  \cup$ \\
 \hspace*{0.63cm} $ \{ (q_s,t_{\rho}),(t_{\rho}, q_s),(q_c,t_{\rho}),(t_{\rho}, q_c), (q_{\rho},t_{\rho}),(t_{\rho}, q_{\rho}) \mid \rho \in \RS, s \in R_{\rho} \cup I_{\rho} \cup P_{\rho} \} 
$

 \item Labels for places in $Q$: 
$$
\begin{array}{c}
L(\Pclock)  = \nat \qquad
  L(q_{\rho})  = \nat  \text{ for each } \rho \in \RS  \\
L(q_s) = [0..\setlev_s-1] \times \nat \times  \nat^{\setlev_s}  \text{ for each } s \in \res 
\end{array}
$$

\item Labels for arcs in $F$:
$$
\begin{array}{llr}
 L((\Pclock, t_c)) = z & L((t_c, \Pclock )) = z'\\
    L((q_s, t_c)) = \tuple{\bool_s, \refr_s, \birth_s} & L((t_c, q_s)) = \tuple{\bool_s', \refr_s', \birth_s'} & \text{ for each } s\in \res
\end{array}
$$
For each reaction $\rho  \in \RS$ and $s \in R_{\rho} \cup I_{\rho} \cup P_{\rho}$:
$$
\begin{array}{llr}
 L((\Pclock, t_{\rho})) = z & L((t_{\rho}, \Pclock )) = z\\
     L((q_s, t_{\rho})) = \tuple{\bool_s, \refr_s, \birth_s} \quad & %& L((t_{\rho}, q_s)) = \tuple{\bool_s, \refr_s, \birth_s} & \text{ for each } s\in R_{\rho}\cup I_{\rho},\\
     L((t_{\rho}, q_s)) = \begin{cases}
                           \tuple{\bool_s, \refr_s, \birth_s} & \text{if } s\notin P_{\rho}\\
                           \tuple{\bool_s', \refr_s', \birth_s'} & \text{otherwise}
                          \end{cases}\\
 
 %    L((q_p, t_{\rho})) = \tuple{\bool_p, \refr_p, \birth_p} & L((t_{\rho}, q_p)) = \tuple{\bool_p', \refr_p', \birth_p'} &  \text{ for each } p \in  P_{\rho},\\
     L((q_{\rho}, t_{\rho})) = w & L((t_{\rho}, q_{\rho} )) = w'
\end{array}
$$



\item Labels for transitions in $T$:
 $$
\begin{array}{lcl}
 L(t_c) &= & (z'=z+1)  \wedge \bigwedge_{s \in \res} C_s,\\
 \text{where}\\
 C_s   &= & (\lev_s = 0 \vee  (z+1) -\refr_s < \life(\lev_s)) \rightarrow \tuple{\lev'_s, \refr'_s, \birth'_s} = \tuple{\lev_s, \refr_s, \birth_s}  \quad \wedge \\            
&& (\lev_s \neq 0 \wedge (z+1) -\refr_s \geq \life(\lev_s)) \rightarrow \\
&&\hspace*{3cm} \tuple{\lev'_s, \refr'_s, \birth'_s} = \tuple{\lev_s-1, z+1, \birth_s\sub{z+1}{\lev_s}}.
\end{array}
 $$

For each reaction $\rho  \in \RS$:
 $$
\begin{array}{lcl}
L(t_{\rho}) \! &=&  w < z  \wedge  w' = z \quad \wedge \\
&& \bigwedge_{(r, \level{r}) \in R_{\rho}}(\lev_r \geq \level{r} \wedge z - \birth[\level{r}] \geq \dur(\rho) )  \quad \wedge\\
&&  \bigwedge_{(i, \level{i}) \in I_{\rho}}(\lev_i < \level{i} \wedge z - \birth[\level{i}] \geq \dur(\rho) )  \quad  \wedge \\


&& \bigwedge_{(p,+) \in P_{\rho}} C_{p+} \wedge  \bigwedge_{(p,-) \in P_{\rho}}C_{p-},\\  
\text{where}  \\

C_{p+} &=& ( \lev_p =\setlev_p -1) \rightarrow   (\tuple{\lev'_p, \refr'_p, \birth'_p} = \tuple{\lev_p, z, \birth_p}) \quad \wedge \\ 
                                  
&& ( \lev_p < \setlev_p -1)  \rightarrow (\tuple{\lev'_p, \refr'_p, \birth'_p} = \tuple{ \lev_p+1, z, \birth_p\sub{z}{\lev_p +1}}) \\
C_{p-} &=&  ( \lev_p = 0) \rightarrow (\tuple{\lev'_p, \refr'_p, \birth'_p} = \tuple{\lev_p, z, \birth_p})  \quad \wedge \\
&& ( \lev_p > 0) \rightarrow (\tuple{\lev'_p, \refr'_p, \birth'_p} = \tuple{\lev_p-1, z, \birth_p\sub{z}{\lev_p}}).
\end{array}
 $$

 

\item For each $q\in Q$, $s\in \res$ and $\rho\in \RS$, the initial marking $M_0$ is:
$$
M_0(q) =
\begin{cases}
 0 & \text{if } q = \Pclock, \\
 0 & \text{if } q = q_{\rho}, \\
 \tuple{\level{s},0,0^{\setlev_s}}& \text{if } q = q_s.
\end{cases}
$$
\end{itemize}

\end{definition}



We now comment on the transitions of the \rnd network. The result of the firing of a transition is handled by  guards (namely transition labels $L(t_c)$ and $L(t_{\rho})$) together with the evaluation $\sigma$ as described after Definition \ref{def:PTS}.   With an abuse of notation, in the following, we refer to evaluated variables without effectively mentioning the evaluation $\sigma$: \ie we say that the current value of the clock is $z$ instead of $\sigma(z)$.
Input and output arcs between the same place and transition with the same label (read arcs) are denoted in figures with a double-pointed arrow with a single label.


\begin{figure}[t]
\centering
\subfigure[Clock transition with only one place $q_s$. \label{fig:clock}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{no place}=[circle,thick,draw=blue!0,fill=blue!0,minimum size=7mm]
 \tikzstyle{red place}=[place,draw=red!75,fill=red!20]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]


  \node [place, label = above: $\Pclock$] at (4,0) (Pc){};
  \node [place, node distance = 4cm, label=above:$q_s$]at (0,0)  (R){};

  \node [transition] (tC) [  label={[red] left:$L(t_{c})$}] at (2,0) {$t_{c}$}
   edge [pre]    node[above] {$z$}    (Pc)
   edge [post,bend right]   node[below]{$z'$}    (Pc)
   edge [pre, bend right]    node[above] {$\tuple{\bool_s,\refr_s,\birth_s}$}    (R)
   edge [post, bend left]    node[auto] {$\tuple{\bool_s',\refr_s',\birth_s'}$}    (R);
  
\end{tikzpicture}
} 
\subfigure[Reaction transition $\rho= (R, I, P)$. \label{fig:reaction}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{no place}=[circle,thick,draw=blue!0,fill=blue!0,minimum size=7mm]
 \tikzstyle{red place}=[place,draw=red!75,fill=red!20]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]



 \node [place, label = right: $q_p$] at (3,0) (P){};
 \node [place, label = above: $\Pclock$] at (0,2) (Pc){};
 \node [place, label = above: $q_r$] at (1,4) (R){};
 \node [place, label = above: $q_i$] at (5,4) (I){};
 \node [place, label = above: $q_{\rho}$] at (6,2) (qw){};
 
 \node [transition, label={[red] right:$L(t_{\rho})$}] at (3,2) (tr) {$t_{\rho}$}
   edge [pre and post]    node[above] {$z$}    (Pc)
   edge [pre and post]    node[left] {$\tuple{\lev_r,\refr_r,\birth_r}$}   (R)
   edge [pre and post]    node[left] {$\tuple{\lev_i,\refr_i,\birth_i}$}     (I)
   edge [pre, bend right]    node[left] {$\tuple{\lev_p,\refr_p,\birth_p}$}   (P)
   edge [post, bend left]   node[below] {$\qquad \qquad \quad \tuple{\lev'_p,\refr'_p,\birth_p'}$}     (P)
   edge [pre, bend left]    node[below] {$w$}   (qw)
   edge [post, bend right]   node[above] {$w'$}     (qw);
   
  
\end{tikzpicture}
}




\end{figure}


Clock transition $t_c$, depicted in Figure \ref{fig:clock}, takes care of Case \ref{item:clock} above. The clock is incremented by one ($z'=z+1$) if guard $L(t_c)$ is satisfied.  Moreover, following Case \ref{item:clock}, $L(t_c)$ is responsible of the decay and the related update of the  level of each species.
If a species $s$ is at  level zero or its last update has occurred less than $\life(\lev_s)$ time units earlier  when compared to the next value $z+1$ of the clock ($(z+1)-\refr_s < \life(\lev_s)$) the content of place $q_s$ remains unchanged.  
Otherwise $s$ decays and behaves as detailed in Case \ref{item:clock}.
%Notice that we choose to compare to the next value  $z+1$ of the clock  to satisfy Assumption (A\ref{item:reclock}).



Next, we describe transitions for reactions, depicted in Figure \ref{fig:reaction}. Given a reaction $\rho=(R,I,P)$ we detail the conditions and the results of firing of $t_{\rho}$. As described in Case \ref{item:reaction} we have:
\begin{itemize}
 \item each reactant $r \in R$ has to be present at least at  level $\level{r}$ for at least $\dur(\rho)$ time units, this is expressed by  guard $\lev_r \geq \level{r} \wedge z - \birth[\level{r}] \geq \dur(\rho) $; 
 \item each inhibitor $i\in I$ has not to exceed  level $\level{i}$ for at least $\dur(\rho)$ time units,  this is guaranteed by guard 
$(\lev_i < \level{i} \wedge z - \birth[\level{i}] \geq \dur(\rho) )$;
\item if a product $p \in P $ has to be increased (respectively decreased) then the corresponding place $q_p$ is updated to $ \tuple{\lev'_p, \refr'_p, \birth'_p} = \tuple{\lev_p+1, z, \birth_p\sub{z}{\lev_p +1}}$ by incrementing its expression level by one (respectively $\tuple{\lev'_p, \refr'_p, \birth'_p} = \tuple{\lev_p-1, z, \birth_p\sub{z}{\lev_p}}$). 
Notice that if  $p$ is already at the maximum (respectively the minimum)  level, only the field $\refr'_p$ is updated to the current value of the clock $z$, all other fields are left unchanged.
\end{itemize}
The role of place $q_{\rho}$ is to retain the timestamps of the last occurence of  reaction $\rho$. This way two consecutive executions of the same reaction are separated by at least one time unit.

Observe that, because of non determinism and interleaving, reaction may not occur even if all time constraints are satisfied, which is interpreted as a circumstance where reactants are too far from each other to react.


\begin{example}
\begin{figure}[t]
\centering
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[rectangle,rounded corners, thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{no place}=[circle,thick,draw=blue!0,fill=blue!0,minimum size=7mm]
 \tikzstyle{red place}=[place,draw=red!75,fill=red!20]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]



 \node [place, label = above: ] at (2,7) (sugar){$Sugar$};
 \node [place, label = above: ] at (6,7) (asp){$Aspartame$};
 \node [place, label = right: ] at (2,4) (glucose){$Glycemia$};
% \node [place, label = right: ] at (5,5) (nt){$Neurotransmitter$};
 %\node [place, label = left: ] at (0,2) (glycog){$Glycogenesis$};
% \node [place, label = right: ] at (4,2) (glycol){$Glycogenolysis$};
 \node [place, label = right: ] at (-2,4) (gluc){$Glucagon$}; 
 \node [place, label = right: ] at (6,4) (ins){$Insulin$}; 
 %\node [place, label = above: ] at (-1,5) (hunger){$Hunger$};
%\node [place, label = below: ] at (6,5) (clock){$Clock$};

\node [transition, label={[red] right:}] at (2,5.5) (tr1) {1}
  edge [pre]    node[left] {R}    (sugar)
  edge [ post]    node[above] {+}   (ins)
  edge [ post]    node[left] {+}   (glucose);
  
\node [transition, label={[red] right:}] at (6,5.5) (tr2) {2}
  edge [pre]    node[left] {R}    (asp)
  edge [post]    node[left] {+}   (ins);

  
  \node [transition, label={[red] right:}] at (0,4) (tr3) {3}
  edge [pre]    node[above] {I}    (glucose)
  edge [ post]    node[above] {+}   (gluc);
  
  
\node [transition, label={[red] right:}] at (4,4) (tr4) {4}
  edge [pre]    node[above] {R}    (glucose)
  edge [post]    node[above] {+}   (ins);
  



 \node [transition, label={[red] right:}] at (4,3) (tr5) {5}
   edge [pre]    node[above] {R}    (ins)
   edge [post]    node[above] {-}   (glucose);
   
   \node [transition, label={[red] right:}] at (4,2) (tr6) {6}
   edge [pre]    node[above] {R}    (glucose)
   edge [pre]    node[above] {R}    (ins)
   edge [post, bend left=30]    node[above] {-}   (glucose);
 

\node [transition, label={[red] right:}] at (4,1) (tr7) {7}
  edge [pre, bend left=35]    node[above] {I}    (glucose)
  edge [pre]    node[right] {R}    (ins)

  edge [post, bend left =60]    node[left] {-}   (glucose);

 
 \node [transition, label={[red] right:}] at (0,3) (tr8) {8}
  edge [pre]    node[below] {R}    (gluc)
  edge [post]    node[below] {+}   (glucose);

\end{tikzpicture}
 \caption{Simplified \rnd network of glucose metabolism. } \label{fig:randyglucose}
\end{figure}


Figure \ref{fig:randyglucose} shows a simplification of the \rnd network $(\res, \RS)$ given in example \ref{ex:glucose}. It focuses only on the reaction schema linking inputs (\ie reactants and inhibitors) to products. 
Each input arc is labeled with either  letter R or letter I denoting whether the input place is a reactant or an inhibitor,  respectively. Likewise, each output arc is labeled with a + or a - to denote increase or decrease of product levels.
For each reaction transition $\rho$, we have omitted the special place $q_{\rho}$ storing the timestamp, all arcs in the opposite direction and all arcs linking the transition to the clock. The clock place, its update transition and its adjacent arcs are omitted as well.
The numbers inside the transition refers to the corresponding reaction in Example \ref{ex:glucose}.

\begin{figure}[ht]
\centering
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,rounded corners, thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

% \node [place, label = right: $Glycogenesis$] at (3,-1) (glycog){};
 \node [place, label = above:$q_{glycemia}$ ] at (0,4) (gl){}; 
 \node [place, label = below: $q_{insulin}$ ] at (0,0) (ins){}; 
 \node [place, label = below:$\qquad \ \Pclock$ ] at (0,2) (clock){};
 \node [place, label = right:$q_{\rho_7}$ ] at (6,2) (qw){};
 
\node [transition, label={[red] left:$L(t_c)$} ] at (-3,2) (tr1) {$t_c$}
  edge [pre ]    node[below] {$z$}    (clock)
  edge [post,bend left=30]    node[below] {$z'$}    (clock)
  edge [pre, bend left ]    node[left] {\ $\quad \tuple{\lev_{gl},\refr_{g},\birth_{g}}$}    (gl)
  edge [post ]    node[right] {$\tuple{\lev'_{g},\refr'_{g},\birth'_{g}}$}    (gl)
  edge [pre, bend right ]    node [left] { $\tuple{\lev_i,\refr_i,\birth_i}$ }    (ins)
  edge [post ]    node[right] {$\ \tuple{\lev'_i,\refr'_i,\birth'_i}$ }    (ins);
  
\node [transition, label={[red] right:$L(t_{\rho_7})$}] at (3,2) (tr8) {$t_{\rho_7}$}
  edge [pre, bend left=30 ]    node[above] {\qquad \quad $\tuple{\lev_g,\refr_g,\birth_g}$}    (gl)
  edge [pre and post]    node[right] {$\ \tuple{\lev_i,\refr_i,\birth_i}$}    (ins)
  edge [pre and post]    node[below] {$z$}    (clock)
  edge [post,bend right]    node[right] {
  $ \tuple{\lev'_{g},\refr'_{g},\birth'_{g}} $}   (gl)
    edge [pre, bend left]    node[below] {$w$}   (qw)
  edge [post,bend right]    node[above] {$w'$}   (qw);
\end{tikzpicture}
 \caption{Portion of  \rnd network of glucose metabolism. } \label{fig:zoomrandyglucose}
\end{figure}


Figure \ref{fig:zoomrandyglucose}, instead, shows a portion of the  complete \rnd network for the glucose metabolism example, focusing only on reaction $\rho_7$ together with the place for clock ($\Pclock$) and the clock update transition. 
\hfill $\diamond$
\end{example}

